<!DOCTYPE html>
<html>
  <head>
    <meta charset='utf-8'>

    <link rel="stylesheet" type="text/css" 
      href="/assets/css/straybirds.css" media="screen" />
    <link rel="stylesheet" type="text/css" 
      href="/assets/css/pygments.css" media="screen" />

    <!-- MathJax Section Start -->

    <script type="text/javascript"
    src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
    </script>
    <script>
        MathJax.Hub.Config({
              tex2jax: {
              skipTags: ['script', 'noscript', 'style', 'textarea', 'pre']
              }
        });
        MathJax.Hub.Queue(function() {
            var all = MathJax.Hub.getAllJax(), i;
            for(i=0; i < all.length; i += 1) {
                all[i].SourceElement().parentNode.className += ' has-jax';
            }
        });
    </script>

    <!-- MathJax Section End -->

    <!-- Google Analytics Start-->
    <script>
  (function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
  (i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
  m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
  })(window,document,'script','//www.google-analytics.com/analytics.js','ga');

  ga('create', 'UA-48100787-1', 'minixalpha.github.io');
  ga('send', 'pageview');

</script>

    <!-- Google Analytics End -->

    <title>内存模型的验证论文阅读</title>
  </head>

  <body>
    <div class="container">
      <header>
        <div class="container">
          <h1>
              <a href="/" title="Home Page"> 潇湘夜雨 </a>
          <span class="github-src">
            <a href ="https://github.com/minixalpha/minixalpha.github.io"
               target="_blank"
               title="Fork me on GitHub">
              <img src="/assets/images/GitHub-Mark-Light-32px.png" alt="">
            </a>
          </span>
          </h1>
        </div>
      </header>

      <aside id="left-side">
        <h2> 分类 </h2>
  <ul class="category-list">
      
            
                <li>
                <a href="/categories/计算机系统"> 计算机系统 (3) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/java"> java (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/技术"> 技术 (5) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/工具"> 工具 (4) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/科研"> 科研 (5) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/生活"> 生活 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/思想"> 思想 (2) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/c语言"> c语言 (4) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/虚拟机"> 虚拟机 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/英语"> 英语 (8) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/读书"> 读书 (1) </a>
                </li>
            
      
            
                <li>
                <a href="/categories/源代码阅读"> 源代码阅读 (10) </a>
                </li>
            
      
  </ul>

      </aside>

      <aside id="right-side">
        <h2> 归档 </h2>
  <ul class="archive-list">
    
    
    
        
        
        
        
            
            <li>
                <a href="/2014/05">
                    2014-05 (1)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/04">
                    2014-04 (3)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/03">
                    2014-03 (11)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/02">
                    2014-02 (6)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2014/01">
                    2014-01 (3)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2013/11">
                    2013-11 (10)
                </a>
            </li>

        
        
    
        
        
        
        
    
        
        
        
        
    
        
        
        
        
            
            <li>
                <a href="/2013/10">
                    2013-10 (3)
                </a>
            </li>

        
        
    
  </ul>

      </aside>

      <article>

<h1>内存模型的验证论文阅读</h1>

<h2>动态验证</h2>

<h3>Hangal2004</h3>

<ul>
<li><p>论文名
Hangal S, Vahia D, Manovit C, et al. TSOtool: A program for verifying memory systems using the memory consistency model[C]//ACM SIGARCH Computer Architecture News. IEEE Computer Society, 2004, 32(2): 114.</p></li>
<li><p>主要内容</p>

<ul>
<li>实现工具TSOtool，用于检测多处理器的共享内存系统</li>
<li>内存模型TSO</li>
<li>随机生成包含data race的程序</li>
<li>提出多项式时间算法，incomplete</li>
<li>检测出商业系统中的设计错误</li>
<li>根据内存模型定义一种次序关系，通过程序及结果构造有向图，
在图中找环</li>
<li>时间复杂度：最坏O(n^5)</li>
</ul></li>
<li><p>参考文献</p>

<ul>
<li>验证SC的复杂度, 将问题定义为VSC, VSC-read(map read to write), VSC-conflict(VSC-read + total order of write): Gibbons P B, Korach E. Testing shared memories[J]. SIAM Journal on Computing, 1997, 26(4): 1208-1244. </li>
</ul></li>
</ul>

<h3>Manovit 2005</h3>

<ul>
<li><p>论文名
Manovit C, Hangal S. Efficient algorithms for verifying memory consistency[C]//Proceedings of the seventeenth annual ACM symposium on Parallelism in algorithms and architectures. ACM, 2005: 245-252.</p></li>
<li><p>主要内容　</p>

<ul>
<li>将vector clock引入TSOtool工具</li>
<li>为VSC-conflict问题提出一个多项式算法</li>
<li>为VSC-read提出多项式算法，快速，有效，但不完备</li>
<li>时间复杂度：O(k*n^3)</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h3>Manovit 2006</h3>

<ul>
<li><p>论文名
Manovit C, Hangal S. Completely verifying memory consistency of test program executions[C]//High-Performance Computer Architecture, 2006. The Twelfth International Symposium on. IEEE, 2006: 166-175.</p></li>
<li><p>主要内容 </p>

<ul>
<li>在TSOtool中引入回溯，使验证TSO内存模型的算法完备</li>
<li>时间复杂度: O(p*n^3)</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h3>Roy 2006</h3>

<ul>
<li><p>论文名
Roy A, Zeisset S, Fleckenstein C J, et al. Fast and generalized polynomial time memory consistency verification[C]//Computer Aided Verification. Springer Berlin Heidelberg, 2006: 503-516.</p></li>
<li><p>主要内容</p>

<ul>
<li>提出新的算法，将最坏时间复杂度降低至O(n^4)，适用于任何占用O(n^2)空间的内存一致性模型</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h3>Chen 2008</h3>

<ul>
<li><p>论文名
Chen Y, Lv Y, Hu W, et al. Fast complete memory consistency verification[C]//High Performance Computer Architecture, 2009. HPCA 2009. IEEE 15th International Symposium on. IEEE, 2009: 381-392.</p></li>
<li><p>主要内容　</p>

<ul>
<li>实现工具LCHECK</li>
<li>引入time order的概念</li>
<li>对可靠完备性验证，时间复杂度O(C^p<em>p^2</em>n^2)</li>
<li>对可靠但不完备性验证，时间复杂度(p^3*n)</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h2>静态验证</h2>

<h3>Park 1995</h3>

<ul>
<li><p>论文名
Park S, Dill D L. An executable specification, analyzer and verifier for RMO (relaxed memory order)[C]//Proceedings of the seventh annual ACM symposium on Parallel algorithms and architectures. ACM, 1995: 34-41.</p></li>
<li><p>主要内容</p>

<ul>
<li>使用murphi语言描述SPARC的RMO内存模型</li>
<li>murphi verifier 可以生成小断汇编语言多处理器程序的所有结果</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h3>Condon 1999</h3>

<ul>
<li><p>论文名
Condon A E, Hill M D, Plakal M, et al. Using lamport clocks to reason about relaxed memory models[C]//High-Performance Computer Architecture, 1999. Proceedings. Fifth International Symposium On. IEEE, 1999: 270-278.</p></li>
<li><p>主要内容</p>

<ul>
<li>对TSO和Alapha内存模型，给出定义，实现，以及对实现的证明</li>
</ul></li>
<li><p>参考文献</p></li>
</ul>

<h3>Chatterjee2002</h3>

<ul>
<li><p>论文名　
Chatterjee P, Sivaraj H, Gopalakrishnan G. Shared memory consistency protocol verification against weak memory models: Refinement via model-checking[C]//Computer Aided Verification. Springer Berlin Heidelberg, 2002: 123-136.</p></li>
<li><p>主要内容</p>

<ul>
<li>设计者需要为具体实现建立一个高度简化的抽象，这层抽象可以用定理证明验证正确性</li>
<li>抽象层和具体实现同时在模型检测工具上运行，检测refinement</li>
<li>验证了四种Alpha内存模型，三种Itanium内存模型</li>
<li>使用并行化的murphi模型检测工具</li>
</ul></li>
</ul>

<h3>Condon 2001</h3>

<ul>
<li><p>论文名
Condon A E, Hu A J. Automatable verification of sequential consistency[J]. Theory of Computing Systems, 2003, 36(5): 431-460.</p></li>
<li><p>主要内容</p>

<ul>
<li>对实现内存系统的有限状态协议进行验证，看是否满足SC</li>
<li>SC基于图定义</li>
<li>协议满足SC当且仅当它的所有trace无环</li>
<li>observer 观察协议执行，收集信息，构造图</li>
<li>图被送给 chekcer ，检查是否有环</li>
<li>如果chekcer接受了observer产生的所有图，那么协议是正确的 </li>
</ul></li>
<li><p>参考文献</p></li>
</ul>


      </article>

      <div class="comments">
        
          <div id="disqus_thread"></div>
 <script type="text/javascript">
     /* * * CONFIGURATION VARIABLES: EDIT BEFORE PASTING INTO YOUR WEBPAGE * * */
     var disqus_shortname = 'minixalpha'; // required: replace example with your forum shortname

     /* * * DON'T EDIT BELOW THIS LINE * * */
     (function() {
         var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true;
         dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js';
         (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq);
     })();
 </script>
 <noscript>Please enable JavaScript to view the <a href="http://disqus.com/?ref_noscript">comments powered by Disqus.</a></noscript>
    <a href="http://disqus.com" class="dsq-brlink">comments powered by <span class="logo-disqus">Disqus</span></a>
    

        
      </div>


      <footer>
        Copyright (c) minixalpha 2014
      </footer>

    </div>
  </body>
</html>
